Nuprl Lemma : ma-single-sends_wf 11,40
k:Knd, l:IdLnk, ds:x:Id fp Type, da:a:Knd fp Type,
f:((tg:Id  (State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List).
with declarations ds:dsda:dak(v) sends f s v on link l  MsgA 
latex

Definitionsx:A. B(x), t  T, with declarations ds:dsda:dak(v) sends f s v on link l, t.1, t.2, x. t(x), x(s)
Lemmasmk-ma wf, fpf-empty wf, Id wf, rationals wf, fpf-cap wf, id-deq wf, ma-state wf, bool wf, Knd wf, ma-valtype wf, pi1 wf, pi2 wf, fpf-single wf, IdLnk wf, Kind-deq wf, rcv wf, finite-prob-space wf, fpf wf

origin